\begin{tabbing}
trigger1\=\{\$trigger:ut2, \$a:ut2, \$x:ut2\}\+
\\[0ex]($T$; $A$; $P$; $i$; $k$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=R{-}base{-}recognize($i$;"\$x" : $A$;"\$trigger";$k$;$T$;$\lambda$$s$,$v$. $P$($s$("\$x"),$v$)) / \+
\\[0ex][Rpre($i$;"\$trigger" : $\mathbb{B}$;"\$a";$\ast$1$\ast$;$\lambda$$s$.$s$("\$trigger")) / []]])
\-
\end{tabbing}